a:, b:. q:. r:int_seg(0; b). (a = ((q * b) + r)) 

latex

Definitions	t  T, x:A. B(x), , x:A. B(x), prop{i:l}, P  Q, decidable(P), int_seg(i; j), , False, P  Q, A  B, A
Lemmas	nat plus wf, decidable le, le wf, quot rem exists n, int seg wf, decidable int equal